1. Field of the Invention
The present invention generally relates to a method and device for automatically testing the correctness of a control system. Particularly, the present invention relates to a method and device for verifying a set of rules in a rule-based expert system.
2. Description of the Related Art
The use of knowledge bases as components within safety or business critical systems has become more and more widespread during the 90s, and has attracted renewed attention in agent based intelligent web-applications. A very common technique to store knowledge in these systems is via rules. This form of expressing knowledge has—amongst others—the advantage that it employs a representation that resembles the way experts tend to express most of their problem solving techniques, namely by situation-action rules.
Most of today's expert systems are rule-based. They consist of a set of condition-action rules, which—taken together—define the overall behavior of the system. Each single rule describes a situation in which a certain action has to take place. For example, in an expert system for E-mail processing, a rule may say that whenever a message for user A is received with a subject containing the word W, it is forwarded to mailbox M on system S.
Small expert systems consisting of just a few dozen of rules and maintained by only one person may well be fully understood without too much effort. But as the number of rules increases, the complexity of the whole system increases disproportionately. Multiple persons working together on the same rule base aggravate this effect. This weighs even more as it is often impossible to partition the rule set into mutually independent groups of rules. The resulting dependencies may lead to unintended behavior, for example, by simultaneously activating two rules with contradictory actions. In such situations, the expert system may enter a loop characterized by oscillation between two or more computation states, which ultimately results in a non-terminating computation.
Thus, in such a case, the expert system gets hung up and does not produce any further answers. Clearly, this has to be avoided, especially when the expert system is used as a component within a safety or business critical computer system.
Due to the high complexity there is a strong potential for errors during the generation and maintenance of rules. In this patent we present a solution to a very common problem of expert systems: the existence of overlapping rules or inconsistently interacting rules, which lead to program cycles or loops. With increasing size of the rule base the detection and avoidance of such faults becomes dramatically harder, and thus has to be handled systematically.
In U.S. Pat. No. 6,063,132 by William Frantz DeCamp et. al., assigned to International Business Machines Corporation, Armonk, N.Y., US, filed Jun. 26, 1998, issued May 16, 2000, “Method for verifying design rule checking software”, design rules for VLSIchip design are verified by repeatedly running predefined checks on these rules. This is only applicable to IC (integrated circuit) design rules, there is no check for consistency of rule systems mentioned.
U.S. Pat. No. 5,559,718 by Allen Baisuck et. al., assigned to Cadence Design Systems, Inc., San Jose, Calif., US, filed Apr. 28, 1994, issued Sep. 24, 1996, “System and method for model-based verification of local design rules”, shows a method to verify properties of ICs composed of different cells, each described by rules of a design model. It checks dependencies between cells, and the cells itself. However, the method is not applicable to rule-based expert systems.
U.S. Pat. No. 6,078,737 by Kyou Suzuki, assigned to NEC Corporation, Tokyo, Japan, filed Sep. 18, 1997, issued Jun. 20, 2000, “Design rule check method”, relates to detection of violation of design rules in IC design, including overlapping rule violations. However, the subject matter is applicable to IC design only, not to general expert system rule bases.
U.S. Pat. No. 5,592,590 by Christopher H. Jolly, assigned to General Electric Company, Schenectady, N.Y., US, filed Jul. 1, 1994, Jan. 7, 1997, “Method for efficiently detecting covered rules in a knowledge base”, teaches a way of detecting of useless rules in a knowledge base. However, no detection of infinite computations is taught, hence, it refers to a different class of errors.
U.S. Pat. No. 5,751,595 by Harry John Beatty et. al., assigned to International Business Machines Corporation, Armonk, N.Y., US, filed Mar. 14, 1996, issued May 12, 1998, “Method for building and verifying authenticity of a rule system”, shows a method to check for unauthorized modification of rule base. However, a detection of errors within rule base is not disclosed.
U.S. Pat. No. 6,108,670 by Robert Anthony Weida et. al., assigned to International Business Machines Corporation, Armonk, N.Y., US, filed Dec. 30, 1998, issued Aug. 22, 2000, “Checking and enabling database updates with a dynamic, multi-modal, rule based system”, describes an update mechanism for databases employing rules. However, no error checking of dynamic aspect of rule system is taught.
U.S. Pat. No. 5,963,739 by Peter Vincent Homeier, Philadelphia, Pa., filed Apr. 25, 1997, issued Oct. 5, 1999, “Method for verifying the total correctness of a program with mutually recursive procedures”, discloses a verification method for procedural programs by building verification conditions based on procedure call graph. However, the discloses method is not applicable to rule bases.
In U.S. Pat. No. 6,175,946 by Tai An Ly et. al., assigned to O-IN Design Automation, San Jose, Calif., US, filed Oct. 20, 1997, issued Jan. 16, 2001, “Method for automatically generating checkers for finding functional defects in a description of a circuit”, descriptions of IC functionality (“checkers”) are automatically generated in order to find errors. This is not applicable to rule bases.
U.S. Pat. No. 5,596,752 by Helge Knudsen et. al., assigned to Amdahl Corporation, Sunnyvale, Calif., US, filed Mar. 11, 1993, issued Jan. 21, 1997, “System for creating, editing, displaying, and executing rules-based programming language rules having action part subsets for both true and false evaluation of the conditional part”, relates to maintenance of rule systems. However, there is no method for error detection within rule system described.
U.S. Pat. No. 5,228,116 by Larry R. Harris, assigned to Aicorp., Inc., Waltham, Mass., US, filed May 17, 1991, issued Jul. 13, 1993, “Knowledge base management system” relates to checking of if-conditions in (COBOL-)programs using an expert system, with rules stored in external data base. However, there is no error detection within rule base.
U.S. Pat. No. 5,826,250 by Alan Trefler, assigned to Pegasystems Inc., Cambridge, Mass., US, filed Jun. 19, 1996, issued Oct. 20, 1998, “Rules bases and methods of access thereof”, relates to a special kind of expert system allowing inheritance of facts. There is no error detection involved.
Grumberg, O., Francez, N., and Makowsky, J. A., “A Proof Rule for Fair Termination of Guarded Commands”, Information and Control 66(1/2):83-102, 1985. This paper describes a highly abstract method to detect non-termination of rule-based programs. The method relies on the generation of a well-founded partial ordering (W, Table 1), but there is no algorithm given for its computation.
Gamble, R. F., Roman, G.-C., Ball, W. E., and Cunningham, H. C., “Applying Formal Verification Methods to Rule-based Programs,” International Journal of Expert Systems: Research and Applications 7(3):203-237, 1994.
Preece, A. D., Grossner, C., and Radhakrishnan, T., “Validating Dynamic Properties of Rule-Based Systems”, International Journal of Human Computer Studies, 44(2):145-169, 1996. Here, a method to check dynamic properties of rule-based systems is presented. It generates an execution graph and examines paths in this graph that correspond to possible program runs. However, only a fraction of possible runs can be covered in reasonable time. Therefore the method cannot, e.g., guarantee the absence of loops.
Thomas J. Laffey, Walton A. Perkins, Deanne Pecora and Tin A. Nguyen, “Knowledge Base Verification” A1 Magazine, AAAI Press, Summer 1987, 69-75.
The examples above showed that a correct definition and the maintenance of rule-based expert systems are hard and error-prone. Considering all possible cases one by one is prohibitive as, for example, a rule set with only 25 (binary) variables generates over 33 million theoretically possible combinations. Therefore, a systematic and automatic methodology has to be applied.
Further related references cited in the System Automation (SA) example hereinafter are as follows:
[GBOO] S. Garone and N. Buck. Capturing, Reusing, and Applying Knowledge for Competitive Advantage: Computer Associate's Aion. International Data Corporation, 2000. IDC White Paper.
[HA99] J. Horl and B. K. Aichernig. Formal specification of a voice communication system used in air traffic control: An industrial application of light-weight formal methods using VDM++. In FM'99-Formal Methods, Vol. II, volume 1709 of Lecture Notes in Computer Science, pages 1868-1868. Springer, 1999.
[Har84] D. Harel. Dynamic logic. In D. Gabbay and F. Guenthner editors, Handbook of Philosophical Logic, volume II: Extensions of Classical Logic, pages 507-544. Kluwer, 1984.
[HS82] D. Harel and R. Sherman R. Sherman. Looping vs. Repeating in dynamic logic. Information and Control, 55(1-3):175-192, 1982.
[KaiOl] A. Kaiser. A SAT-based prepositional prover for consistency checking of automotive product data. Technical report, Wilhelm-Schickard-Institut fur Informatik, Eberhard-Karls-Universitat Tubingen, Sand 13, 72076 Tubingen, Germany, 2001. Technical Report WSI-2001-16.
[KMS96] H. Kautz. D. McAllester, and B. Selman. Encoding plans in prepositional logic. In Proc. Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), pages 374-384, Cambridge, Mass., November 1996, Morgan Kaufmann.
[SGBOO] S. Spreeuwenberg/, R. Gerrits, and M. Boekenoogen. VALENS: A Knowledge Based Tool to Validate and Verify an Aion Knowledge Base. In ECAI 2000, 14th European Conference on Artificial Intelligence, pages 731-735. IDS Press, 2000.
[Som98] F. Somenzl. CUDD: CU Decision Diagram Package, Release 2.3.0. University of Colorado, Boulder, 1998. Available at http://vlsi.colorado.edu/fabio.
[Str82] R. S. Streett. Propositional dynamic logic of looping and converse is elementarily decidable, Information and Control, 54(1/2): 121-141, 1982.